<html>
<head><meta charset="utf-8"><title>Trait solver in Coq · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html">Trait solver in Coq</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="234026810"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234026810" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234026810">(Apr 11 2021 at 08:19)</a>:</h4>
<p>Any interests in doing a formal version of the solver in theorem provers like Coq? I see similar things being mentioned in the Chalk pages</p>



<a name="234028283"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234028283" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234028283">(Apr 11 2021 at 08:45)</a>:</h4>
<p>That's a good question for which I'd like to hear the answer as well. Although, I would expect that the lowering process and the resulting clauses, that essentially encode Rusts trait system, would make a better formalization target than the solvers themselves.</p>



<a name="234124266"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234124266" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234124266">(Apr 12 2021 at 08:50)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq/near/234028283">said</a>:</p>
<blockquote>
<p>That's a good question for which I'd like to hear the answer as well. Although, I would expect that the lowering process and the resulting clauses, that essentially encode Rusts trait system, would make a better formalization target than the solvers themselves.</p>
</blockquote>
<p>Thanks. I think it would interesting to see a formallisation of the trait system in coq would look like</p>



<a name="234294984"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234294984" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234294984">(Apr 13 2021 at 09:32)</a>:</h4>
<p><span class="user-mention silent" data-user-id="389506">kentrixy</span> <a href="#narrow/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq/near/234026810">said</a>:</p>
<blockquote>
<p>Any interests in doing a formal version of the solver in theorem provers like Coq? I see similar things being mentioned in the Chalk pages</p>
</blockquote>
<p>Any more interests in this?<br>
 :)</p>



<a name="234390327"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234390327" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234390327">(Apr 13 2021 at 19:56)</a>:</h4>
<p>If it's been talked about, it would have been discussed before I was around. I'm not 100% what additional benefit we would get. I think longer-term, we want to essentially try to distill the Rust trait system in to a set of clauses (as Chalk does) and write that formally. Currently, there are some things that we can't express solely as clauses; it would be interesting if we <em>could</em> one day, but not sure. I think either way, trying to do a "formal version" is several years off</p>



<a name="234431172"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234431172" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234431172">(Apr 14 2021 at 02:18)</a>:</h4>
<p>I think writing a formal statement of the trait system is very valuable, whether it's written in Coq, as datalog clauses, or something else, and proving things about that statement is not a requirement. It's a necessary component of eventual specification, and certainly it will make it easier for people who want to try proving something about the system to have a basis on which to work with some reasonable connection to the real thing</p>



<a name="234431316"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234431316" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234431316">(Apr 14 2021 at 02:20)</a>:</h4>
<p>I don't think it is a several years project. A month sounds about right, but that's assuming the actual semantics are known. The most likely stalling point would be in areas where no one knows what we actually want to do and we hesitate to certify what rustc currently does as official</p>



<a name="234437864"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234437864" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234437864">(Apr 14 2021 at 04:00)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq/near/234431172">said</a>:</p>
<blockquote>
<p>I think writing a formal statement of the trait system is very valuable, whether it's written in Coq, as datalog clauses, or something else, and proving things about that statement is not a requirement. It's a necessary component of eventual specification, and certainly it will make it easier for people who want to try proving something about the system to have a basis on which to work with some reasonable connection to the real thing</p>
</blockquote>
<p>Thanks. I believe such a system would not be a multi year project either. What I'd like to think is how such a formal system would be of help to the language designer/compiler people. However, With no formal spec of Rust language itself, it can be quite a open problem.</p>



<a name="234442968"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Trait%20solver%20in%20Coq/near/234442968" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Trait.20solver.20in.20Coq.html#234442968">(Apr 14 2021 at 05:25)</a>:</h4>
<p>The obvious utility of formalizing these things to language designer / compiler people is that it requires asking hard questions about what to do in various edge cases that may not have been considered, as well as drawing a high level picture of the situation that may reveal certain design inconsistencies that were not originally obvious at the individual-bug-fixes level</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>